x:Id, k:Knd, ds:x:Id fp Type, da:a:Knd fp Type, f:(State(ds)Valtype(da;k)ds(x)?Void).
xdom(ds). A=ds(x)   A
 kdom(da). A=da(k)   A
 xdom(ds). A=ds(x)   AtomFree(Type;A)
 kdom(da). A=da(k)   AtomFree(Type;A)
 Feasible(with declarations 
 ds:ds
 da:da
 effect of k(v) is x := f s v) 

latex

Definitions

t  T, P  Q, x:A. B(x), b, f(x), x  dom(f), xdom(f). v=f(x)   P(x;v), Type, AtomFree(T;x), f(a), Dec(P), x:AB(x), a:A fp B(a), 1of(t), Id, type List, 2of(t), Knd, KindDeq, deq-member(eq;x;L), IdDeq, IdLnk, False, false, <a,b>, product-deq(A;B;a;b), eqof(d), p  q, P & Q, (x  l), State(ds), z != f(x)  P(a;z), M.sframe(k sends <l,tg>), M.frame(k affects x), f(x)?z, Feasible(M), mk-ma, , x : v, with declarations ds:dsda:daeffect of k(v) is x := f s v, x. t(x), Void, x.A(x), Valtype(da;k), x:AB(x), Top, {x:A| B(x) }, Prop, x,y. t(x;y), nat-deq-aux, NatDeq, atom-deq-aux, AtomDeq, #$n, a<b, A, AB, , , Atom, prod-deq(A;B;a;b), proddeq(a;b), IdLnkDeq, sum-deq(A;B;a;b), sumdeq(a;b), union-deq(A;B;a;b), P  Q, left+right, P  Q

Lemmas

assert-deq-member, not wf, l member wf, atom-free wf, fpf-all wf, fpf-dom wf, fpf-trivial-subtype-top, ma-state wf, ma-valtype wf, fpf-cap wf, fpf wf, bor wf, eqof wf, product-deq wf, bfalse wf, false wf, IdLnk wf, id-deq wf, Id wf, assert wf, deq-member wf, Kind-deq wf, Knd wf